Issue2883.agda:33,19-20
Σ (El box) (λ x → El ((λ { [ a ] → box }) x)) !=< Nat of type Set
when checking that the expression p has type Nat
